the_es:ES, e', e:E, l:IdLnk. (e  rcvs(l;before(e')))  (e <loc e') & haslnk(l;e) 

latex

Definitions	ES, IdLnk, rcvs(l;before(e')), filter(P;l), before(e), haslnk(l;e), Prop, t  T, (x  l), E, x:A. B(x), P  Q, P  Q, P  Q, b, (e <loc e'), P & Q
Lemmas	assert wf, member-es-before, and functionality wrt iff, iff functionality wrt iff, es-locl wf, es-haslnk wf, l member wf, es-before wf, filter wf, member filter, IdLnk wf, es-E wf, event system wf